Lift

Quite a lot of the time we won't be dealing with booleans, but with <#186#>predicates<#186#>, which are just functions that return a boolean. For example, the predicate Lessthan is defined below so that #math113#Lessthan~i~j is true whenever i ;SPMlt; j. Given a predicate p we would like to be able to <#187#>lift<#187#> it to Lift~p, defined:

#math114#
Lift~p~f~g~x = p~x~f~g~x  

For example, #math115#Lift~(Lessthan~0)~f~g takes in a number and applies f to it if it is positive and g to it otherwise. This is quite useful for defining functions.